|
|
Vizualizace rezoluční metody
Smetka, Tomáš ; Orság, Filip (oponent) ; Rozman, Jaroslav (vedoucí práce)
Tato bakalářská práce se zabývá problematikou automatického dokazování ve výrokové a predikátové logice. V teoretické části je popsána výroková a predikátová logika v návaznosti na systém jejich automatického dokazování pomocí rezoluční metody. V práci je dále popsán návrh a implementace programu, který se skládá z terminálu a serverové části. Program hledá důkaz nesplnitelnosti zadané formule a vizualizuje jednotlivé kroky vedoucí k nalezení řešení. V závěru je vyhodnocena implementace řešení a práce jako celek a také jsou popsány další možnosti rozšíření.
|
|
|
Expertní systémy ES pro samostatné studium a jeho vyhodnocení
Novák, Jaroslav ; Honzík, Petr (oponent) ; Jirsík, Václav (vedoucí práce)
Tato diplomová práce obsahuje základní informace ohledně znalostních a expertních systémů. Dále se zde zabývám architekturou expertních systémů a důkladně jsou zde popsány způsoby reprezentace znalostí pro expertní systémy. Ke každému způsobu reprezentace znalostí jsou zde zpracovány demonstrující jednotlivé způsoby reprezentace znalostí. Na závěr je zde popsán vytvořený expertní systém, který ukládá znalosti pomocí rámcové reprezentace znalostí.
|
|
|
Reprezentace znalostí pro expertní systémy
Lekeš, Pavel ; Sáblík, Václav (oponent) ; Polách, Petr (vedoucí práce)
Tato práce se zabývá možností použití predikátové logiky pro dedukci v systémech umělé inteligence. Výhody logiky prvního řádu jsou zejména v její relativně jednoduché algoritmizaci, kdy lze rozhodnout o platnosti či splnitelnosti věty zapsané pomocí predikátové logiky pouze pomocí formálních pravidel, tedy bez jakékoliv vazby na skutečné denotáty jednotlivých proměnných. V Expertních systémech se predikátová logika využívá k odvození pravdivých formulí ze zadaných axiomů, přičemž se do odvozování zahrnou i nově odvozené pravdivé formule. Jedná se o proces vyhledávání implicitních znalostí z explicitně zadaných axiomů.
|
|
|
Metody reprezentace znalostí
Verbík, Josef ; Polách, Petr (oponent) ; Jirsík, Václav (vedoucí práce)
Práce pojednává o metodách reprezentace znalostí v expertních systémech. V práci jsou charakterizovány expertní systémy a jejich historie. Dále jsou popsány jednotlivé druhy expertních systémů a jeho části. Hned za tímto popisem je charakterizována reprezentace znalostí. Tato charakteristika je rozdělena na dvě části. V první části jsou popsány požadavky pro efektivní reprezentaci znalostí. Ve druhé části jsou popsány jednotlivé metody znalostí. Jsou to pravidla, rámce, sémantické sítě a predikátová logika.
|
|
|
Resolution Method Visualisation
Kasem, Jakub ; Zbořil, František (oponent) ; Rozman, Jaroslav (vedoucí práce)
This bachelor thesis is focused on the topic of automated reasoning using the resolution method. The theoretical part of the thesis focuses on predicate logic, its operations and laws, the resolution method and its processes, state space search by uninformed algorithms, and tools for automated reasoning programming. The thesis further describes the implementation of a educational application visualizing the resolution method. The application automatically proves the truth value of a given statement by finding a contradiction between the negation of the statement and the set of premises and reveals the solution procedure. In the conclusion of the thesis, the implementation of the solution and the content of the work are evaluated and possible improvements are suggested.
|
|
|
Vizualizace rezoluční metody
Smetka, Tomáš ; Orság, Filip (oponent) ; Rozman, Jaroslav (vedoucí práce)
Tato bakalářská práce se zabývá problematikou automatického dokazování ve výrokové a predikátové logice. V teoretické části je popsána výroková a predikátová logika v návaznosti na systém jejich automatického dokazování pomocí rezoluční metody. V práci je dále popsán návrh a implementace programu, který se skládá z terminálu a serverové části. Program hledá důkaz nesplnitelnosti zadané formule a vizualizuje jednotlivé kroky vedoucí k nalezení řešení. V závěru je vyhodnocena implementace řešení a práce jako celek a také jsou popsány další možnosti rozšíření.
|
|
|
Reprezentace znalostí pro expertní systémy
Lekeš, Pavel ; Sáblík, Václav (oponent) ; Polách, Petr (vedoucí práce)
Tato práce se zabývá možností použití predikátové logiky pro dedukci v systémech umělé inteligence. Výhody logiky prvního řádu jsou zejména v její relativně jednoduché algoritmizaci, kdy lze rozhodnout o platnosti či splnitelnosti věty zapsané pomocí predikátové logiky pouze pomocí formálních pravidel, tedy bez jakékoliv vazby na skutečné denotáty jednotlivých proměnných. V Expertních systémech se predikátová logika využívá k odvození pravdivých formulí ze zadaných axiomů, přičemž se do odvozování zahrnou i nově odvozené pravdivé formule. Jedná se o proces vyhledávání implicitních znalostí z explicitně zadaných axiomů.
|
|
|
Metody reprezentace znalostí
Verbík, Josef ; Polách, Petr (oponent) ; Jirsík, Václav (vedoucí práce)
Práce pojednává o metodách reprezentace znalostí v expertních systémech. V práci jsou charakterizovány expertní systémy a jejich historie. Dále jsou popsány jednotlivé druhy expertních systémů a jeho části. Hned za tímto popisem je charakterizována reprezentace znalostí. Tato charakteristika je rozdělena na dvě části. V první části jsou popsány požadavky pro efektivní reprezentaci znalostí. Ve druhé části jsou popsány jednotlivé metody znalostí. Jsou to pravidla, rámce, sémantické sítě a predikátová logika.
|
|
|
Expertní systémy ES pro samostatné studium a jeho vyhodnocení
Novák, Jaroslav ; Honzík, Petr (oponent) ; Jirsík, Václav (vedoucí práce)
Tato diplomová práce obsahuje základní informace ohledně znalostních a expertních systémů. Dále se zde zabývám architekturou expertních systémů a důkladně jsou zde popsány způsoby reprezentace znalostí pro expertní systémy. Ke každému způsobu reprezentace znalostí jsou zde zpracovány demonstrující jednotlivé způsoby reprezentace znalostí. Na závěr je zde popsán vytvořený expertní systém, který ukládá znalosti pomocí rámcové reprezentace znalostí.
|
|
|
NCMPL 2011 Abstracts
Cintula, Petr ; Ju, S. ; Víta, Martin
This volume contains (extended) abstracts of all 6 invited and 25 contributed talks presented at the conference Non-Classical Modal and Predicate Logics which took place in Guangzhou, December 5-9, 2011. Modalities and predicates have since ancient time been central notions in logic. In the 20th century, various systems of non-classical logics have emerged, with applications in many disciplines like Computer Science, Linguistics, Mathematics, and Philosophy. This gave rise to the questions of non-classical treatment of quantification and modalities and their accommodation in these non-classical settings. In response, various modal and predicate variants of non-classical logics have been introduced and studied in the past decades. Although there are many good conferences on (mainly propositional) non-classical logics, this conference was solely dedicated to modal and predicate non-classical logics. Its aim was to bring together esearchers from various branches of non-classical logics, not only to present recent advances in their particular fields, but also to identify common problems and methods and foster the exchange of ideas between researchers from separate fields.
|
host ::
RSS.